A, B:MsgA, l:IdLnk, tg:Id.
rcv(l,tg) declared in A  B  rcv(l,tg) declared in A  rcv(l,tg) declared in B 

latex

Definitions	Id, IdLnk, M1  M2, rcv(l,tg) declared in M, mk-ma, MsgA, Valtype(da;k), KindDeq, f  g, Top, a:A fp B(a), x. t(x), Prop, x  dom(f), rcv(l,tg), Knd, t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, P  Q, b
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, Knd wf, rcv wf, top wf, fpf-join wf, Kind-deq wf, fpf-join-dom, iff functionality wrt iff, msga wf, IdLnk wf, Id wf